package ch.epfl.lara.matcheck.verify.transform;

import ch.epfl.lara.matcheck.ast._

import scala.collection.immutable.HashMap


/**
 * Translate a pattern into a formula.
 */
object Pattern2Formula extends AbstractConversion2Formula {
 
  /**
   * <p>
   *         Apply the translation.
   * </p>
   *
   * @param scrutinee: The scrutinee's name of the matching expression
   * @param pattern  : The pattern to translate
   * @return         : A formula that is equivalent to the pattern
   */
  def apply(scrutinee: String, pattern: PatternDef): Formula = {
     generated_names = Nil
     Convert(scrutinee,pattern)
  }
  
  private object Convert {
  
    // String constant to prepend to any extractor object name
    import ch.epfl.lara.matcheck.Constants._
    import ch.epfl.lara.matcheck.util.Substitute
  
    /**
     * <p>
     * 	Recursively apply the transformation to all subelements of the pattern.
     * </p>
     * 
     * @param variable: Is the variable name assigned to the analyzed pattern.
     * @param pattern : The pattern to translate. 
     * @return        : A formula that is equivalent to the pattern.
     */
    def apply(variable: String, pattern: PatternDef): Imply = {
      var lhs_f: Formula = Tru; var rhs_f: Formula = Tru
    
      def split(variable: String, pattern: PatternDef): Unit = pattern match {
        case Wildcard => ()
        case VarPattern(name,tpe) =>
          lhs_f = And(lhs_f,Eq(Element(variable),Element(name.getName)))
          rhs_f = And(rhs_f, In(Element(variable),Set(tpe.toString)))
          append_name(name.getName)
        case ClassPattern(objname,args) =>
          val args_name = for(pattern<-args) yield pattern match {
            case Wildcard => freshName("wildcard")  
            case ClassPattern(name,_) =>
              freshName(name.getName.toLowerCase) 
              
            case VarPattern(name,_) =>
              append_name(name.getName)
              name.getName
          }
      
          val MethodSymbol(_,paramsTpe,resTpe,ppc) = objname.sym match {
            case null => throw new Exception("Object "+objname+" has not been declared")
            case sym => sym.lookupMethod(UNAPPLY) match {
              case None => throw new Exception(objname+" doesn't have an unapply method")
              case Some(m) => m
            }
          }
           
          assert(paramsTpe.size == 1) // Extractors have exactly one parameter

          val (objName,_) = paramsTpe.head
          
          objname.getSym.lookupMethod(Constants.UNAPPLY).get.ppc match {
            case None => ()
            case Some((_,post)) => 
              val env = (objName,variable) :: args_name.zipWithIndex.map({case (arg_name,index) => ("res"+(index+1),arg_name)})
              lhs_f = And(lhs_f, Substitute(env,post))
          }
          
        
        
          val domaine = DOM_PREPEND+objname.getName  
          rhs_f = And(rhs_f, In(Element(variable),Set(domaine)))
          
          val extractor_fct_name = EXTR_PREPEND+objname.getName

          for(i<-List.range(0,args_name.size)) {
            lhs_f = And(lhs_f, 
                        Eq(Function(extractor_fct_name+SEP+(i+1),List(Element(variable))),
                           Element(args_name(i))
                        )
                      )
            split(args_name(i),args(i))
          }
        }
      split(variable,pattern)
      Imply(lhs_f,rhs_f)
    }
  }
}
